#include <nanobdd.h>

#include <algorithm>
#include <iostream>
#include <map>

namespace nanobdd {

// Bdd::Bdd(int level, std::shared_ptr<Bdd> low, std::shared_ptr<Bdd> high)
//     : level_(level), low_(low), high_(high) {}

bool
Bdd::isFalse() const {
  return node_ == Nanobdd::falseNode;
}

bool
Bdd::isTrue() const {
  return node_ == Nanobdd::trueNode;
}

Bdd
Bdd::negCof(int id) const {
  // check id <= root_
  if (id < level()) {
    return node_;
  } else { // id == root_
    return node_->low();
  }
}

Bdd
Bdd::posCof(int id) const {
  // check id <= root_
  if (id < level()) {
    return node_;
  } else { // id == root_
    return node_->high();
  }
}

Bdd
Bdd::operator&(const Bdd& r) const {
  if (node_ == r.node()) {
    return node_;
  }
  if (isFalse() || r.isFalse()) {
    return Nanobdd::falseNode;
  }
  if (isTrue()) {
    return r;
  }
  if (r.isTrue()) {
    return node_;
  }
  int x = std::min(level(), r.level());

  auto hash = TRIPLEp(0, node_, r.node()) % Nanobdd::cacheSize;
  auto cached = Nanobdd::cache_.lookup(hash, 0, node_, r.node());
  if (cached) {
    return cached;
  }

  auto fLow = negCof(x) & r.negCof(x);
  auto fHigh = posCof(x) & r.posCof(x);

  auto res = combine(x, fLow, fHigh, 0);

  Nanobdd::cache_.insert(hash, res.node(), 0, node_, r.node());

  return res;
}

Bdd
Bdd::operator|(const Bdd& r) const {
  if (node_ == r.node()) {
    return node_;
  }
  if (isTrue() || r.isTrue()) {
    return Nanobdd::getTrueNode();
  }
  if (isFalse()) {
    return r;
  }
  if (r.isFalse()) {
    return node_;
  }
  int x = std::min(level(), r.level());

  auto hash = TRIPLEp(1, node_, r.node()) % Nanobdd::cacheSize;
  auto cached = Nanobdd::cache_.lookup(hash, 1, node_, r.node());
  if (cached) {
    return cached;
  }

  auto fLow = negCof(x) | r.negCof(x);
  auto fHigh = posCof(x) | r.posCof(x);

  auto res = combine(x, fLow, fHigh, 1);

  Nanobdd::cache_.insert(hash, res.node(), 1, node_, r.node());

  return res;
}

Bdd
Bdd::operator!() const {
  if (isTrue()) {
    return Nanobdd::getFalseNode();
  }
  if (isFalse()) {
    return Nanobdd::getTrueNode();
  }

  auto hash = TRIPLEp(2, node_, nullptr) % Nanobdd::cacheSize;
  auto cached = Nanobdd::cache_.lookup(hash, 2, node_, nullptr);
  if (cached) {
    return cached;
  }

  int x = level();
  auto fLow = !negCof(x);
  auto fHigh = !posCof(x);

  auto res = combine(x, fLow, fHigh, 2);

  Nanobdd::cache_.insert(hash, res.node(), 2, node_, nullptr);

  return res;
}

Bdd
Bdd::combine(size_t x, const Bdd& low, Bdd& high, uint32_t opcode) {
  if (low == high) {
    return low;
  }
  return Nanobdd::makeNode(x, low.node(), high.node());
}

} // namespace nanobdd